P1:(es_realizer{i:l}prop{i':l}). 
P1(Rnone)
 (left,right:es_realizer{i:l}. P1(left)  P1(right)  P1(Rplus(left; right)))
 (loc:Id, T:Type{i}, x:Id, v:(T + (rationalsT)). P1(Rinit(loc; T; x; v)))
 (loc:Id, T:Type{i}, x:Id, L:(Knd List). P1(Rframe(loc; T; x; L)))
 (lnk:IdLnk, tag:Id, L:(Knd List). P1(Rsframe(lnk; tag; L)))
 (loc:Id, ds:fpf(Id; x.Type{i}), knd:Knd, T:Type{i}, x:Id,
 (f:((decl-state(ds)Tdecl-type{i:l}
 (f:((decl-state(ds)Tdecl-type(ds; x)) + (decl-state(ds)Trationalsdecl-type{i:l}
 (f:((decl-state(ds)Tdecl-type(ds; x)) + (decl-state(ds)Trationalsdecl-type(ds; x))).
 P1(Reffect(loc; ds; knd; T; x; f)))
 (ds:fpf(Id; x.Type{i}), knd:Knd, T:Type{i}, l:IdLnk, dt:fpf(Id; x.Type{i}),
 (g:((tg:Id  (decl-state(ds)T(decl-type{i:l}(dt; tg) List))) List).
 P1(Rsends(ds; knd; T; l; dt; g)))
 (loc:Id, ds:fpf(Id; x.Type{i}), a:Id, p:finite-prob-space, P:(decl-state(ds)).
 P1(Rpre(loc; ds; a; p; P)))
 (loc:Id, k:Knd, L:(Id List). P1(Raframe(loc; k; L)))
 (loc:Id, k:Knd, L:(IdLnk List). P1(Rbframe(loc; k; L)))
 (loc,x:Id, L:(Knd List). P1(Rrframe(loc; x; L)))
 guard((x1:es_realizer{i:l}. P1(x1))) 

latex

Definitions	x. t(x), t  T, guard(T), x(s), P  Q, prop{i:l}, x:A. B(x), Unit, Rrframe(loc; x; L), Rbframe(loc; k; L), Raframe(loc; k; L), Rpre(loc; ds; a; p; P), Rsends(ds; knd; T; l; dt; g), Reffect(loc; ds; knd; T; x; f), Rsframe(lnk; tag; L), Rframe(loc; T; x; L), Rinit(loc; T; x; v), Rplus(left; right), Rnone, es_realizer{i:l},
Lemmas	Rnone wf, Rplus wf, Rinit wf, Rframe wf, Rsframe wf, Reffect wf, Rsends wf, Rpre wf, Raframe wf, Rbframe wf, Rrframe wf, es realizer wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf